$\forall$${\it ds}$:Top, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$, $T$:Top, ${\it ks}$:Knd List, ${\it tr}$:Top, $j$, $i$:Id.
\\[0ex]R{-}da(R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$);$j$)
\\[0ex]$=$
\\[0ex]if $i$ = $j$$\rightarrow$ reduce($\lambda$$k$,$d_{1}$. $k$ : Valtype(${\it da}$;$k$) $\oplus$ $d_{1}$;;${\it ks}$) else  fi
\\[0ex]$\in$ $k$:Knd fp$\rightarrow$ Type